StandardDS  DS({1..6}) 

latex

Definitions	DS(A), StandardDS, i=j, IdLnk, i  j < k, AB, False, if b t else f fi, Id, {i..j}, EqDecider(T), Unit, P  Q, P & Q, P  Q, IdLnkDeq, , b, Prop, A, b, x:A. B(x), t  T, IdDeq
Lemmas	id-deq wf, assert wf, not wf, bnot wf, idlnk-deq wf, bool wf, assert of eq int, not functionality wrt iff, assert of bnot, iff transitivity, eqff to assert, eqtt to assert, deq wf, int seg wf, ifthenelse wf, Id wf, IdLnk wf, eq int wf